|
Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clauses. An example of a clause including a constraint is A(X,Y) :- X+Y>0, B(X), C(Y) . In this clause, X+Y>0 is a constraint; A(X,Y) , B(X) , and C(Y) are literals as in regular logic programming. This clause states one condition under which the statement A(X,Y) holds: X+Y is greater than zero and both B(X) and C(Y) are true.As in regular logic programming, programs are queried about the provability of a goal, which may contain constraints in addition to literals. A proof for a goal is composed of clauses whose bodies are satisfiable constraints and literals that can in turn be proved using other clauses. Execution is performed by an interpreter, which starts from the goal and recursively scans the clauses trying to prove the goal. Constraints encountered during this scan are placed in a set called constraint store. If this set is found out to be unsatisfiable, the interpreter backtracks, trying to use other clauses for proving the goal. In practice, satisfiability of the constraint store may be checked using an incomplete algorithm, which does not always detect inconsistency. ==Overview== Formally, constraint logic programs are like regular logic programs, but the body of clauses can contain constraints, in addition to the regular logic programming literals. As an example, X>0 is a constraint, and is included in the last clause of the following constraint logic program.B(X,1):- X<0. B(X,Y):- X=1, Y>0. A(X,Y):- X>0, B(X,Y). Like in regular logic programming, evaluating a goal such as A(X,1) requires evaluating the body of the last clause with Y=1 . Like in regular logic programming, this in turn requires proving the goal B(X,1) . Contrary to regular logic programming, this also requires a constraint to be satisfied: X>0 , the constraint in the body of the last clause (in regular logic programming, X>0 cannot be proved unless X is bound to a fully-ground term and execution of the program will fail if that is not the case).Whether a constraint is satisfied cannot always be determined when the constraint is encountered. In this case, for example, the value of X is not determined when the last clause is evaluated. As a result, the constraint X>0 is not satisfied nor violated at this point. Rather than proceeding in the evaluation of B(X,1) and then checking whether the resulting value of X is positive afterwards, the interpreter stores the constraint X>0 and then proceeds in the evaluation of B(X,1) ; this way, the interpreter can detect violation of the constraint X>0 during the evaluation of B(X,1) , and backtrack immediately if this is the case, rather than waiting for the evaluation of B(X,1) to conclude.In general, the evaluation of a constraint logic program proceeds like for a regular logic program, but constraints encountered during evaluation are placed in a set called constraint store. As an example, the evaluation of the goal A(X,1) proceeds by evaluating the body of the first clause with Y=1 ; this evaluation adds X>0 to the constraint store and requires the goal B(X,1) to be proved. While trying to prove this goal, the first clause is applicable, but its evaluation adds X<0 to the constraint store. This addition makes the constraint store unsatisfiable, and the interpreter backtracks, removing the last addition from the constraint store. The evaluation of the second clause adds X=1 and Y>0 to the constraint store. Since the constraint store is satisfiable and no other literal is left to prove, the interpreter stops with the solution X=1, Y=1 .抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)』 ■ウィキペディアで「Constraint logic programming」の詳細全文を読む スポンサード リンク
|